Inference at * 1 
Iof proof for Lemma linorder lt neg:



1. T : Type
2. R : TT
3. x, y:T. Dec(R(x,y))
4. a:T. R(a,a)
5. a, b, c:T. R(a,b)  R(b,c)  R(a,c)
6. x, y:T. R(x,y)  R(y,x)  (x = y)
7. x, y:T. R(x,y)  R(y,x)
8. a : T
9. b : T
  ((R(a,b) & (R(b,a))))  R(b,a) 

latex

 by ((Unfold `decidable` 3 THEN InstHyp [b;a] 3 
THENM InstHyp [a;b] 7 
THENM ProveProp) 

THECollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
TH) inil_term))) 

latex

TH.

Definitions	P  Q, t  T, P & Q, A, P  Q, P  Q, x(s1,s2), , False, P  Q, Dec(P), x:A. B(x)
Lemmas	not wf